A long-standing problem in the design of large-scale, highly complex systems is verifying that the system will behave in the manner intended by its designers. One approach to this problem is to simply try out the system, either by building and testing the system itself or by building and testing a model of the system. Since most new systems require several revisions or redesigns before they behave as intended by the system designer, many system designers choose to first build and test a model of the system. This enables the designer to check the system design by testing the behavior of the system model so that any causes for system redesign can be identified before incurring the expenses associated with building the system itself.
In one method of building and testing a system model, called computer simulation, a designer "builds" the system model by writing a computer program that simulates the intended properties (i.e. functions and features) of the system. The computer program, or system model, is designed to accept inputs, perform functions and generate outputs in the same manner as would the actual system. In computer simulation, the system model is tested by running a checking program which checks how the system model behaves in response to various inputs. Basically, the checking program controls the inputs to the system model, and checks whether the behavior of the model to a given set of inputs is the behavior intended by the system designer. For example, in checking a model of a telephone, a checking program would be operable to control the various telephone model inputs (e.g. AC power level, control signals, and dialed numbers), and monitor the behavior of the telephone model in response to such inputs.
A significant problem with computer simulation, however, is that only the behaviors anticipated by the designer can be checked. That is, the designer can only check those behaviors which the checking program is designed to check. This is a problem because a designer may not posses the system knowledge that is necessary to anticipate or incorporate all of the intended system behaviors into the checking program. Notwithstanding this, even a designer knowledgeable about the system design may find it hard to anticipate some behavioral attributes of a sufficiently complex system. As a result, computer simulation is not always a reliable method of testing the properties (i.e. intended functions and features) of a system design.
As the limitations of simulation have become apparent, interest has grown in another method of building and testing a system model, called formal verification. In formal verification, to test a model of a system, a designer is required to "build" both a system model, which may be the same model used for simulation, and a system design specification. The designer may "build" the system model by writing a computer program or a set of logical expressions that define an implementation of the system, and may "build" the system design specification by writing a set of logical expressions that define the intended behavioral attributes of the system. Basically, the system model is designed to accept inputs, perform functions and generate outputs in the same manner as would the actual system, if built, and the system design specification is designed such that each logical expression defines an intended behavioral attribute of the system or system model.
With a system model and a system design specification, a verification tool can be used to test whether the behavior of the system model is consistent with the intended behaviors defined by the design specification. Often, this is done by converting both the system model and the system design specification into a state machine. The system model state machine can be described as a system or set of states and transitions that reflects or mimics how the system model would behave in response to any given set of inputs. The system design specification state machine can be described as a system or a set of states and transitions that defines how the designer intends or expects the system model to act in response to a given set of inputs. For example, the design specification state machine might define which states the system model state machine may enter (i.e. "good" states) and may not enter (i.e. "bad" states) during operation, when given a certain set of inputs. Thus, to test whether the system model behaves according to the expected behaviors defined in the design specification, the verification tool would control and/or vary the inputs to the system model state machine and check whether the system model state machine can possibly enter any states defined by the design specification state machine as "bad" states. If so, the system design is said to fail the system design specification, and a system redesign may be in order.
Thus, it is clear that the accuracy and reliability of a formal verification system directly depends on the accuracy of the designer in writing the logical expressions that define the system design specification. If the logical expressions do not accurately define the intended behaviors of the system, the design specification state machine will not accurately define which states the system model state machine may and may not enter, given a set of inputs. Moreover, if the design specification state machine fails to accurately define the bad states, then any formal verification test will fail to check the system model for the intended behavior. Thus, the reliability of formal verification ultimately depends on the accuracy of the designer in writing the logical expressions that define the system design specification.
Heretofore, when writing the logical expressions that define a system design specification, designers are literally faced with the task of working from a blank page. That is, the designers must decide how to express each intended behavioral attribute beginning with a blank page and a set of logical operators. To illustrate, most present day designers use temporal logic to write the required logical expressions. A temporal logic expression can be generated by using a set of temporal logic operators which may include "G" meaning "at every state", "F" meaning "eventually", "A" meaning "along all state transition executions, ".about." meaning "not", meaning "or", and ".fwdarw." meaning "implies." Thus, to generate a logical expression that defines a given intended behavioral attribute of the system, the designer must understand the logical meaning of each operator, decide which operators to use, and decide how to associate the chosen operators with the appropriate system variables or system parameters to ultimately form an expression of the behavior being defined.
For example, temporal logic can be used to express a behavioral attribute such as turning on an oven when a temperature goes below a certain value. One temporal logic designer may express this behavior as AG(t.fwdarw.AF(.about.p w)), where the parameter "t" means the temperature goes below the stated value, "p" means the oven is powered, and "w" means the oven is turned on. Another designer, however, may decide that this behavior could be expressed in temporal logic as G(t.fwdarw.F(w)), wherein the parameters "t" and "w" are the same as described above. Although each expression may appear to its respective designer as accurately defining the system behavior, the expressions do not have the same logical meaning and thus do not define the same system behavior. As a result, it is very possible that different designers can write completely different logical expressions for defining the same system property, with one logical expression not actually defining the same intended behavior as the other. Thus, unless the designer posses both a detailed knowledge of the system design and a high level of skill in the logic being used to define the design specification, use of conventional formal verification tools to test a system design can be quite difficult and unreliable.